COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	SPECIAL I_ANTECEDENT, I_MATCHLIST, I_REJECTEDGOALS, I_GOALDEPTH, I_GOALDEPTHMAX,
C00007 ENDMK
C⊗;
SPECIAL I_ANTECEDENT, I_MATCHLIST, I_REJECTEDGOALS, I_GOALDEPTH, I_GOALDEPTHMAX,
	I_GOALIST;
EXPR INFER1(CONSEQUENCE);
	BEGIN
	%
	INFER0 is the main logical routine - and recursively tears apart the
	consequence until it decides that it is ready to prove some subpart is
	derivable from the antecedent/inference rules/rejectedgoals list at
	which point it calls INFER2.

	INFER1 returns the simplified consequence.
	%
	NEW RESULT, REJECTS, SAVEDMATCHLIST, TEMP;
	
	IF NULL CONSEQUENCE THEN RETURN NIL;
	IF ATOM CONSEQUENCE THEN RETURN INFER2(CONSEQUENCE);

	IF CAR CONSEQUENCE = '?#AND
		% Every conjunct is proved in turn.  If one is unprovable, then
		  the effort switch is made NIL, overriding the value given it
		  by the user's call to INFER.   The rationale is that if something
		  is known to be unprovable, why waste too much time on the rest
		  of the formula?
		%
		THEN FOR NEW X IN CDR CONSEQUENCE DO
			BEGIN
			RESULT ← INFER1(X);
			IF RESULT
				THEN REJECTS ← REJECTS @ DELETESYM('?#AND,RESULT)
				ALSO I_EFFORT ← 'GIVEN;
			END
		ALSO RETURN REPLACESYM('?#AND, REJECTS);

	IF CAR CONSEQUENCE = '?#OR
		% Given a consequence A #OR B, we first try to prove A #OR B directly
		  from the antecedent (hence the immediate call too INFER2).   If
		  that fails, we try in succession to prove A and then B from the
		  antecedent.   Notice the stacking and unstacking of the matchlist
		  as we try to prove successive disjuncts; rather more trickily 
		  notice the lack of stacking and unstacking of the rejectedgoalslist
		  and updated antecedent as we try to prove successive disjuncts.
		  The correctness of this requires more argument than I have the
	 	  patience to give at the moment.
		%

		THEN RESULT ← INFER2(CONSEQUENCE)
		ALSO IF NULL RESULT THEN RETURN NIL
		
		ELSE SAVEDMATCHLIST ← I_MATCHLIST
		
		ALSO FOR NEW X IN CDR CONSEQUENCE DO
			BEGIN
			I_MATCHLIST ← SAVEDMATCHLIST;
			RESULT ← INFER1(X);
			REJECTS ← REJECTS @ DELETESYM('?#OR,RESULT)
			END
		UNTIL RESULT = NIL

		ALSO IF RESULT
			THEN I_MATCHLIST ← SAVEDMATCHLIST
			ALSO RETURN REPLACESYM('?#OR, REJECTS)
			ELSE RETURN NIL;

	IF CAR CONSEQUENCE = '?#IMPLY
		% We rely on the mechanism of INFER0.   But for this case only,
		  we have to roll back the rejectedgoals list - since we are
		  adding stuff to the antecedent, it may be no longer true that
	 	  everything in the rejectedgoals list is unprovable.
		%
		THEN I_REJECTEDGOALS ← NIL
		ALSO RETURN INFER0(CONSEQUENCE[2], CONSEQUENCE[3]);

	% We have recursed down far enough on the formula and have run out
	  of logical connectives.   Time to call INFER2.
	%
	RETURN INFER2(CONSEQUENCE);
	END;

_EOF_